g:OMon, a, b:|g|. (a  b)  ((a < b)  (a = b)) 

latex

Up	groups 1
Definitions of Statement	gset, goset, a  b, a < b
Definitions	t  T, x:A. B(x), t.2, t.1, , gset, LOSet, goset, a  b, |p|, a < b, a  b
Lemmas	omon wf, loset wf, oset of ocmon wf, set leq iff lt or eq